Search for: All records

Exact probabilistic inference is a requirement for many applications of probabilistic programming languages (PPLs) such as in high-consequence settings or verification. However, designing and implementing a PPL with scalable high-performance exact inference is difficult: exact inference engines, much like SAT solvers, are intricate low-level programs that are hard to implement. Due to this implementation challenge, PPLs that support scalable exact inference are restrictive and lack many features of general-purpose languages. This paper presents Roulette, the first discrete probabilistic programming language that combines high-performance exact inference with general-purpose language features. Roulette supports a significant subset of Racket, including data structures, first-class functions, surely-terminating recursion, mutable state, modules, and macros, along with probabilistic features such as finitely supported discrete random variables, conditioning, and top-level inference. The key insight is that there is a close connection between exact probabilistic inference and the symbolic evaluation strategy of Rosette. Building on this connection, Roulette generalizes and extends the Rosette solver-aided programming system to reason about probabilistic rather than symbolic quantities. We prove Roulette sound by generalizing a proof of correctness for Rosette to handle probabilities, and demonstrate its scalability and expressivity on a number of examples. 

Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, this paper proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature. 

In Detroit, the largest Black-majority city in the United States, municipal authorities have deployed an array of surveillance technologies with the promise of containing crime and improving community safety. This article draws from a cross-sectional survey of over two thousand Detroit residents and multi-year community-based fieldwork in Detroit’s Eastside to examine local perceptions of policing surveillance technologies. Our survey reveals that respondents, notably those in more vulnerable positions, report higher perceived safety levels with policing surveillance cameras in their neighborhoods. However, when triangulating these results with insights from our fieldwork, we argue that these survey findings should not be taken as public support for surveillance. Alongside this seeming buy-in is a widely shared “better than nothing” imaginary among residents from impacted communities. “Better than nothing,” for the residents, is a pragmatic compromise and maneuver between being aware of the inherent flaws of surveillance technologies and settling for any available resource or hope. This notion of “better than nothing” unveils residents’ prolonged wait for digital justice and institutional accountability, which we show is where racialized infrastructural harm and exploitation are enacted along the temporal dimension. Our findings offer practical insights for counter-surveillance advocacy efforts. 

Abstract The Knuth–Morris–Pratt (KMP) algorithm for string search is notoriously difficult to understand. Lost in a sea of index arithmetic, most explanations of KMP obscure its essence. This paper constructs KMP incrementally, using pictures to illustrate each step. The end result is easier to comprehend. Additionally, the derivation uses only elementary functional programming techniques. 

Software contracts empower programmers to describe functional properties of components. When it comes to constraining effects, though, the literature offers only one-off solutions for various effects. It lacks a universal principle. This paper presents the design of an effectful contract system in the context of effect handlers. A key metatheorem shows that contracts cannot unduly interfere with a program’s execution. An implementation of this design, along with an evaluation of its generality, demonstrates that the theory can guide practice. 

For more than two decades, functional programmers have refined the persistent red-black tree—a data structure of unrivaled elegance. This paper presents another step in its evolution. Using a monad to communicate balancing information yields a fast insertion procedure, without sacrificing clarity. Employing the same monad plus a new decomposition simplifies the deletion procedure, without sacrificing efficiency. 

Abstract Behavioral software contracts allow programmers to strengthen the obligations and promises that they express with conventional types. They lack expressive power, though, when it comes to invariants that hold across several function calls. Trace contracts narrow this expressiveness gap. A trace contract is a predicate over the sequence of values that flow through function calls and returns. This paper presents a principled design, an implementation, and an evaluation of trace contracts. 

Noticing differently commits to stepping out of familiar reference frameworks while attending to oft-neglected actors, relations, and ways of knowing for design. Photovoice is an arts- and community-based participatory approach allowing individuals to communicate their lives and stories about pressing community concerns through photography. This paper bridges photovoice and the commitment to noticing in HCI and design through a photovoice project with Detroit residents on safety and surveillance. The photovoice process—alongside the production, reflection, and dissemination of photographs—makes residents’ everyday situations legible and sensible, allowing both community members and researchers to orient to and engage with multiple viewpoints, sensibilities, and temporal trajectories. This process confronts the invisibility of both the sociotechnical infrastructures (in our case, surveillance infrastructures) and minoritized communities’ relational ontologies. By advocating participatory noticing in design research, we show the opportunities for adopting arts- and community-based participatory approaches in decentering dominant ways of knowing and seeing, while at the same time fostering community capacity and relations for future potentialities. 

Safety has been used to justify the expansion of today’s large-scale surveillance infrastructures in American cities. Our work offers empirical and theoretical groundings on why and how the safety-surveillance conflation that reproduces harm toward communities of color must be denaturalized. In a photovoice study conducted in collaboration with a Detroit community organization and a university team, we invited 11 Black mid-aged and senior Detroiters to use photography to capture their lived experiences of navigating personal and community safety. Their photographic narratives unveil acts of “everyday noticing” in negotiating and maintaining their intricate and interdependent relations with human, non-human animals, plants, spaces, and material things, through which a multiplicity of meaning and senses of safety are produced and achieved. Everyday noticing, as simultaneously a survival skill and a more-than-human care act, is situated in residents’ lived materialities, while also serving as a site for critiquing the reductive and exclusionary vision embedded in large-scale surveillance infrastructures. By proposing an epistemological shift from surveillance-as-safety to safety-through-noticing, we invite future HCI work to attend to the fluid and relational forms of safety that emerge from local entanglement and sensibilities. 

Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries between typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the viability of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead. Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of a program. We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead—with a median overhead of 2.5× and up to 80.6× in the worst case—and eliminate all overhead in most cases, suffering only 1.5× overhead in the worst case.